Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U611(tt, V) → U621(isPalListKind(activate(V)), activate(V))
U911(tt, V2) → ACTIVATE(V2)
ISNELIST(V) → ACTIVATE(V)
U541(tt, V1, V2) → ISNELIST(activate(V1))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
U721(tt, P) → U731(isPal(activate(P)), activate(P))
ACTIVATE(n__o) → O
U811(tt, V) → ACTIVATE(V)
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
U821(tt, V) → ISNEPAL(activate(V))
U311(tt, V) → U321(isPalListKind(activate(V)), activate(V))
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U711(tt, I, P) → ACTIVATE(I)
ISPAL(V) → ACTIVATE(V)
U611(tt, V) → ISPALLISTKIND(activate(V))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U431(tt, V1, V2) → ACTIVATE(V2)
U241(tt, V1, V2) → ISLIST(activate(V1))
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U211(tt, V1, V2) → ACTIVATE(V2)
U811(tt, V) → ISPALLISTKIND(activate(V))
U731(tt, P) → ACTIVATE(P)
ISLIST(V) → ISPALLISTKIND(activate(V))
U431(tt, V1, V2) → ACTIVATE(V1)
U121(tt, V) → ISNELIST(activate(V))
U541(tt, V1, V2) → ACTIVATE(V1)
U231(tt, V1, V2) → ACTIVATE(V1)
U221(tt, V1, V2) → ACTIVATE(V1)
U551(tt, V2) → U561(isList(activate(V2)))
U511(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U821(tt, V) → U831(isNePal(activate(V)))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U531(tt, V1, V2) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
U911(tt, V2) → U921(isPalListKind(activate(V2)))
U111(tt, V) → ACTIVATE(V)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U221(tt, V1, V2) → ACTIVATE(V2)
U241(tt, V1, V2) → ACTIVATE(V2)
U211(tt, V1, V2) → ISPALLISTKIND(activate(V1))
ISNEPAL(V) → U611(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → ACTIVATE(V1)
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U531(tt, V1, V2) → ACTIVATE(V2)
ISLIST(n____(V1, V2)) → ACTIVATE(V1)
U251(tt, V2) → ACTIVATE(V2)
U221(tt, V1, V2) → ISPALLISTKIND(activate(V2))
ISNEPAL(V) → ISPALLISTKIND(activate(V))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U321(tt, V) → ACTIVATE(V)
U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISLIST(V) → ACTIVATE(V)
U421(tt, V1, V2) → ACTIVATE(V2)
U251(tt, V2) → ISLIST(activate(V2))
U441(tt, V1, V2) → ACTIVATE(V1)
U111(tt, V) → ISPALLISTKIND(activate(V))
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)
U511(tt, V1, V2) → ACTIVATE(V2)
ISNEPAL(n____(I, n____(P, I))) → ISQID(activate(I))
U451(tt, V2) → ACTIVATE(V2)
U551(tt, V2) → ACTIVATE(V2)
U121(tt, V) → U131(isNeList(activate(V)))
U241(tt, V1, V2) → ACTIVATE(V1)
U231(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U731(tt, P) → U741(isPalListKind(activate(P)))
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V2)
U311(tt, V) → ISPALLISTKIND(activate(V))
U611(tt, V) → ACTIVATE(V)
ISNEPAL(n____(I, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
U411(tt, V1, V2) → ISPALLISTKIND(activate(V1))
U721(tt, P) → ACTIVATE(P)
U431(tt, V1, V2) → ISPALLISTKIND(activate(V2))
__1(__(X, Y), Z) → __1(Y, Z)
U451(tt, V2) → ISNELIST(activate(V2))
U521(tt, V1, V2) → ACTIVATE(V2)
ACTIVATE(n__nil) → NIL
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V1)
U421(tt, V1, V2) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U621(tt, V) → U631(isQid(activate(V)))
U211(tt, V1, V2) → ACTIVATE(V1)
U621(tt, V) → ISQID(activate(V))
U711(tt, I, P) → ACTIVATE(P)
ISLIST(n____(V1, V2)) → ACTIVATE(V2)
U441(tt, V1, V2) → ISLIST(activate(V1))
ACTIVATE(n__i) → I
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
ACTIVATE(n__e) → E
ISPAL(V) → ISPALLISTKIND(activate(V))
U421(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → ACTIVATE(V2)
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U121(tt, V) → ACTIVATE(V)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
ISNEPAL(n____(I, n____(P, I))) → ACTIVATE(I)
ISNEPAL(V) → ACTIVATE(V)
U251(tt, V2) → U261(isList(activate(V2)))
U541(tt, V1, V2) → ACTIVATE(V2)
U311(tt, V) → ACTIVATE(V)
U551(tt, V2) → ISLIST(activate(V2))
U321(tt, V) → ISQID(activate(V))
ACTIVATE(n__a) → A
U411(tt, V1, V2) → ACTIVATE(V2)
ISNEPAL(n____(I, n____(P, I))) → ACTIVATE(P)
ISNELIST(n____(V1, V2)) → ACTIVATE(V1)
U511(tt, V1, V2) → ISPALLISTKIND(activate(V1))
ACTIVATE(n__u) → U
U521(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U821(tt, V) → ACTIVATE(V)
ACTIVATE(n____(X1, X2)) → __1(activate(X1), activate(X2))
ISNELIST(V) → ISPALLISTKIND(activate(V))
U521(tt, V1, V2) → ACTIVATE(V1)
U531(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U731(tt, P) → ISPALLISTKIND(activate(P))
ISLIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U711(tt, I, P) → ISPALLISTKIND(activate(I))
ISNELIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U721(tt, P) → ISPAL(activate(P))
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
ISNELIST(V) → U311(isPalListKind(activate(V)), activate(V))
U441(tt, V1, V2) → ACTIVATE(V2)
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
U321(tt, V) → U331(isQid(activate(V)))
U621(tt, V) → ACTIVATE(V)
U231(tt, V1, V2) → ACTIVATE(V2)
U451(tt, V2) → U461(isNeList(activate(V2)))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U611(tt, V) → U621(isPalListKind(activate(V)), activate(V))
U911(tt, V2) → ACTIVATE(V2)
ISNELIST(V) → ACTIVATE(V)
U541(tt, V1, V2) → ISNELIST(activate(V1))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
U721(tt, P) → U731(isPal(activate(P)), activate(P))
ACTIVATE(n__o) → O
U811(tt, V) → ACTIVATE(V)
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
U821(tt, V) → ISNEPAL(activate(V))
U311(tt, V) → U321(isPalListKind(activate(V)), activate(V))
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U711(tt, I, P) → ACTIVATE(I)
ISPAL(V) → ACTIVATE(V)
U611(tt, V) → ISPALLISTKIND(activate(V))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U431(tt, V1, V2) → ACTIVATE(V2)
U241(tt, V1, V2) → ISLIST(activate(V1))
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U211(tt, V1, V2) → ACTIVATE(V2)
U811(tt, V) → ISPALLISTKIND(activate(V))
U731(tt, P) → ACTIVATE(P)
ISLIST(V) → ISPALLISTKIND(activate(V))
U431(tt, V1, V2) → ACTIVATE(V1)
U121(tt, V) → ISNELIST(activate(V))
U541(tt, V1, V2) → ACTIVATE(V1)
U231(tt, V1, V2) → ACTIVATE(V1)
U221(tt, V1, V2) → ACTIVATE(V1)
U551(tt, V2) → U561(isList(activate(V2)))
U511(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U821(tt, V) → U831(isNePal(activate(V)))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U531(tt, V1, V2) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
U911(tt, V2) → U921(isPalListKind(activate(V2)))
U111(tt, V) → ACTIVATE(V)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U221(tt, V1, V2) → ACTIVATE(V2)
U241(tt, V1, V2) → ACTIVATE(V2)
U211(tt, V1, V2) → ISPALLISTKIND(activate(V1))
ISNEPAL(V) → U611(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → ACTIVATE(V1)
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U531(tt, V1, V2) → ACTIVATE(V2)
ISLIST(n____(V1, V2)) → ACTIVATE(V1)
U251(tt, V2) → ACTIVATE(V2)
U221(tt, V1, V2) → ISPALLISTKIND(activate(V2))
ISNEPAL(V) → ISPALLISTKIND(activate(V))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U321(tt, V) → ACTIVATE(V)
U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISLIST(V) → ACTIVATE(V)
U421(tt, V1, V2) → ACTIVATE(V2)
U251(tt, V2) → ISLIST(activate(V2))
U441(tt, V1, V2) → ACTIVATE(V1)
U111(tt, V) → ISPALLISTKIND(activate(V))
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)
U511(tt, V1, V2) → ACTIVATE(V2)
ISNEPAL(n____(I, n____(P, I))) → ISQID(activate(I))
U451(tt, V2) → ACTIVATE(V2)
U551(tt, V2) → ACTIVATE(V2)
U121(tt, V) → U131(isNeList(activate(V)))
U241(tt, V1, V2) → ACTIVATE(V1)
U231(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U731(tt, P) → U741(isPalListKind(activate(P)))
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V2)
U311(tt, V) → ISPALLISTKIND(activate(V))
U611(tt, V) → ACTIVATE(V)
ISNEPAL(n____(I, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
U411(tt, V1, V2) → ISPALLISTKIND(activate(V1))
U721(tt, P) → ACTIVATE(P)
U431(tt, V1, V2) → ISPALLISTKIND(activate(V2))
__1(__(X, Y), Z) → __1(Y, Z)
U451(tt, V2) → ISNELIST(activate(V2))
U521(tt, V1, V2) → ACTIVATE(V2)
ACTIVATE(n__nil) → NIL
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V1)
U421(tt, V1, V2) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U621(tt, V) → U631(isQid(activate(V)))
U211(tt, V1, V2) → ACTIVATE(V1)
U621(tt, V) → ISQID(activate(V))
U711(tt, I, P) → ACTIVATE(P)
ISLIST(n____(V1, V2)) → ACTIVATE(V2)
U441(tt, V1, V2) → ISLIST(activate(V1))
ACTIVATE(n__i) → I
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
ACTIVATE(n__e) → E
ISPAL(V) → ISPALLISTKIND(activate(V))
U421(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → ACTIVATE(V2)
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U121(tt, V) → ACTIVATE(V)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
ISNEPAL(n____(I, n____(P, I))) → ACTIVATE(I)
ISNEPAL(V) → ACTIVATE(V)
U251(tt, V2) → U261(isList(activate(V2)))
U541(tt, V1, V2) → ACTIVATE(V2)
U311(tt, V) → ACTIVATE(V)
U551(tt, V2) → ISLIST(activate(V2))
U321(tt, V) → ISQID(activate(V))
ACTIVATE(n__a) → A
U411(tt, V1, V2) → ACTIVATE(V2)
ISNEPAL(n____(I, n____(P, I))) → ACTIVATE(P)
ISNELIST(n____(V1, V2)) → ACTIVATE(V1)
U511(tt, V1, V2) → ISPALLISTKIND(activate(V1))
ACTIVATE(n__u) → U
U521(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U821(tt, V) → ACTIVATE(V)
ACTIVATE(n____(X1, X2)) → __1(activate(X1), activate(X2))
ISNELIST(V) → ISPALLISTKIND(activate(V))
U521(tt, V1, V2) → ACTIVATE(V1)
U531(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U731(tt, P) → ISPALLISTKIND(activate(P))
ISLIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U711(tt, I, P) → ISPALLISTKIND(activate(I))
ISNELIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
U721(tt, P) → ISPAL(activate(P))
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
ISNELIST(V) → U311(isPalListKind(activate(V)), activate(V))
U441(tt, V1, V2) → ACTIVATE(V2)
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
U321(tt, V) → U331(isQid(activate(V)))
U621(tt, V) → ACTIVATE(V)
U231(tt, V1, V2) → ACTIVATE(V2)
U451(tt, V2) → U461(isNeList(activate(V2)))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 5 SCCs with 97 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ RuleRemovalProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))

The TRS R consists of the following rules:

activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
u → n__u
o → n__o
i → n__i
e → n__e
a → n__a
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)
nil → n__nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))

Strictly oriented rules of the TRS R:

isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X

Used ordering: POLO with Polynomial interpretation [25]:

POL(ISPALLISTKIND(x1)) = 2 + 2·x1   
POL(U91(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U911(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U92(x1)) = x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 0   
POL(activate(x1)) = x1   
POL(e) = 0   
POL(i) = 0   
POL(isPalListKind(x1)) = 2 + 2·x1   
POL(n____(x1, x2)) = 2 + 2·x1 + x2   
POL(n__a) = 0   
POL(n__e) = 0   
POL(n__i) = 0   
POL(n__nil) = 0   
POL(n__o) = 0   
POL(n__u) = 1   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 1   
POL(u) = 1   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
              ↳ QDP
                ↳ RuleRemovalProof
                  ↳ QDP
                    ↳ DependencyGraphProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))

The TRS R consists of the following rules:

activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
U92(tt) → tt
u → n__u
o → n__o
i → n__i
e → n__e
a → n__a
__(X1, X2) → n____(X1, X2)
nil → n__nil

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U721(tt, P) → ISPAL(activate(P))
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
ISNEPAL(n____(I, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
U821(tt, V) → ISNEPAL(activate(V))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
ISNEPAL(n____(I, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
The remaining pairs can at least be oriented weakly.

ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U721(tt, P) → ISPAL(activate(P))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
U821(tt, V) → ISNEPAL(activate(V))
Used ordering: Polynomial interpretation with max and min functions [25]:

POL(ISNEPAL(x1)) = x1   
POL(ISPAL(x1)) = x1   
POL(U711(x1, x2, x3)) = 1 + x2 + x3   
POL(U721(x1, x2)) = x2   
POL(U811(x1, x2)) = x2   
POL(U821(x1, x2)) = x2   
POL(U91(x1, x2)) = 0   
POL(U92(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(activate(x1)) = x1   
POL(e) = 0   
POL(i) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(n____(x1, x2)) = 1 + x1 + x2   
POL(n__a) = 0   
POL(n__e) = 0   
POL(n__i) = 0   
POL(n__nil) = 0   
POL(n__o) = 1   
POL(n__u) = 0   
POL(nil) = 0   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 0   

The following usable rules [17] were oriented:

o → n__o
__(__(X, Y), Z) → __(X, __(Y, Z))
i → n__i
activate(n__nil) → nil
u → n__u
activate(n__a) → a
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__i) → i
activate(n__e) → e
activate(n__u) → u
activate(n__o) → o
activate(X) → X
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
__(X, nil) → X
e → n__e
__(nil, X) → X



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ DependencyGraphProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U721(tt, P) → ISPAL(activate(P))
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
U821(tt, V) → ISNEPAL(activate(V))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 4 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U451(tt, V2) → ISNELIST(activate(V2))
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U541(tt, V1, V2) → ISNELIST(activate(V1))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U551(tt, V2) → ISLIST(activate(V2))
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
U251(tt, V2) → ISLIST(activate(V2))
U121(tt, V) → ISNELIST(activate(V))
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))
The remaining pairs can at least be oriented weakly.

U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U451(tt, V2) → ISNELIST(activate(V2))
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U541(tt, V1, V2) → ISNELIST(activate(V1))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U551(tt, V2) → ISLIST(activate(V2))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
U251(tt, V2) → ISLIST(activate(V2))
U121(tt, V) → ISNELIST(activate(V))
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
Used ordering: Polynomial interpretation [25]:

POL(ISLIST(x1)) = x1   
POL(ISNELIST(x1)) = x1   
POL(U11(x1, x2)) = 0   
POL(U111(x1, x2)) = x2   
POL(U12(x1, x2)) = 0   
POL(U121(x1, x2)) = x2   
POL(U13(x1)) = 0   
POL(U21(x1, x2, x3)) = 0   
POL(U211(x1, x2, x3)) = 1 + x2 + x3   
POL(U22(x1, x2, x3)) = 0   
POL(U221(x1, x2, x3)) = 1 + x2 + x3   
POL(U23(x1, x2, x3)) = 0   
POL(U231(x1, x2, x3)) = x2 + x3   
POL(U24(x1, x2, x3)) = 0   
POL(U241(x1, x2, x3)) = x2 + x3   
POL(U25(x1, x2)) = 0   
POL(U251(x1, x2)) = x2   
POL(U26(x1)) = 0   
POL(U31(x1, x2)) = 0   
POL(U32(x1, x2)) = 0   
POL(U33(x1)) = 0   
POL(U41(x1, x2, x3)) = 0   
POL(U411(x1, x2, x3)) = x2 + x3   
POL(U42(x1, x2, x3)) = 0   
POL(U421(x1, x2, x3)) = x2 + x3   
POL(U43(x1, x2, x3)) = 0   
POL(U431(x1, x2, x3)) = x2 + x3   
POL(U44(x1, x2, x3)) = 0   
POL(U441(x1, x2, x3)) = x2 + x3   
POL(U45(x1, x2)) = 0   
POL(U451(x1, x2)) = x2   
POL(U46(x1)) = 0   
POL(U51(x1, x2, x3)) = 0   
POL(U511(x1, x2, x3)) = 1 + x2 + x3   
POL(U52(x1, x2, x3)) = 0   
POL(U521(x1, x2, x3)) = x2 + x3   
POL(U53(x1, x2, x3)) = 0   
POL(U531(x1, x2, x3)) = x2 + x3   
POL(U54(x1, x2, x3)) = 0   
POL(U541(x1, x2, x3)) = x2 + x3   
POL(U55(x1, x2)) = 0   
POL(U551(x1, x2)) = x2   
POL(U56(x1)) = 0   
POL(U91(x1, x2)) = 0   
POL(U92(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(activate(x1)) = x1   
POL(e) = 0   
POL(i) = 0   
POL(isList(x1)) = 0   
POL(isNeList(x1)) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(n____(x1, x2)) = 1 + x1 + x2   
POL(n__a) = 0   
POL(n__e) = 0   
POL(n__i) = 0   
POL(n__nil) = 0   
POL(n__o) = 0   
POL(n__u) = 0   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   

The following usable rules [17] were oriented:

o → n__o
i → n__i
activate(n__nil) → nil
u → n__u
activate(n__a) → a
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__i) → i
activate(n__e) → e
activate(n__u) → u
activate(n__o) → o
activate(X) → X
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U451(tt, V2) → ISNELIST(activate(V2))
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U541(tt, V1, V2) → ISNELIST(activate(V1))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U551(tt, V2) → ISLIST(activate(V2))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U121(tt, V) → ISNELIST(activate(V))
U251(tt, V2) → ISLIST(activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 21 less nodes.